FDL - Nuprl Lemma : generated-thread-properties2

Nuprl Lemma : generated-thread-properties2

es:ES, P:(E

), R:(E

E

).
single-thread-generator{i:l}(es;P;R)

(

e, e':E. (R(e,e'))

(P(e) & P(e')))

((

e, e':E. P(e)

P(e')

(((e R^+ e')

(e = e'))

(e' R^+ e)))

c

(

x, y:E. (P(x) & P(y))

((R^+(x,y))

(x < y)))

c

(

x, y:E. (R(x,y))

(R^+!(x,y)))

c

(

x, y, x', y':E. (R^+(x,y))

(R(y',y))

((R^+(x,y'))

(x = y')))

c

(

x, y, x', y':E. (R^+(x,y))

(R(x',x))

(R(y',y))

(R^+(x',y'))))

Definitions R|P, E <>{T} E', x(s), ES, , Type, single-thread-generator{i:l}(es;P;R), A c B, R!, P Q, (e < e'), P Q, left + right, s = t, x f y, R^+, x:A. B(x), P & Q, x:A B(x), f(a), E, P Q, x:AB(x), connex(T;R), Connex(T;x,y.R(x;y)), R^*, {T}, P Q, x. t(x)

Lemmas implies functionality wrt iff, all functionality wrt iff, rel-star-iff-rel-plus-or, or functionality wrt iff, generated-thread-binrel-properties2